Inhalt des Dokuments

Diplom

Formal Verification of a Broadcast-Free Consensus Algorithm in Isabelle

Donnerstag, 13. September 2012

Erstgutachter/in: Prof. Dr.-Ing. Nestmann
Zweitgutachter/in: Dr. Kammüller

Jin, Qiang

In Isabelle wurde ein weit verbreiteter Consensus-Algorithmus formal verifiziert.  Die Aufgabe besteht darin eine Variante dieses Algorithmus ebenfalls in Isabelle zu verifizieren und dabei auf das Prinzip der Wiederverwendbarkeit von Beweisen zu achten und eventuell die existierenden Beweise zu adaptieren.

---